M.rframe(k reads x) == L != (M.2.2.2.2.2.2.2.2.2.2).1(x)  deq-member(KindDeq;k;L) 

latex

---

clarification:

M.rframe(k reads x)
== fpf-val(IdDeq; ((M.2.2.2.2.2.2.2.2.2.2).1); x; x,L.(deq-member(KindDeq;k;L))) 

latex

Definitions	z != f(x)  P(a;z), IdDeq, t.1, t.2, b, deq-member(eq;x;L), KindDeq
FDL editor aliases	ma-rframe